import gmp.Mpq;

import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;

import apron.Abstract1;
import apron.ApronException;
import apron.Box;
import apron.Environment;
import apron.Interval;
import apron.Linexpr1;
import apron.Linterm1;
import apron.Manager;
import apron.MpqScalar;
import soot.Local;
import soot.Unit;
import soot.Value;
import soot.ValueBox;
import soot.jimple.AddExpr;
import soot.jimple.DivExpr;
import soot.jimple.IntConstant;
import soot.jimple.MulExpr;
import soot.jimple.NegExpr;
import soot.jimple.ParameterRef;
import soot.jimple.SubExpr;
import soot.jimple.ThisRef;
import soot.jimple.internal.AbstractJimpleIntBinopExpr;
import soot.jimple.internal.JAssignStmt;
import soot.jimple.internal.JGeExpr;
import soot.jimple.internal.JGtExpr;
import soot.jimple.internal.JIdentityStmt;
import soot.jimple.internal.JIfStmt;
import soot.jimple.internal.JLeExpr;
import soot.jimple.internal.JLtExpr;
import soot.jimple.internal.JReturnStmt;
import soot.jimple.internal.JimpleLocal;
import soot.util.Chain;
import soot.toolkits.graph.UnitGraph;
import soot.toolkits.scalar.ForwardBranchedFlowAnalysis;


public class IntervalAnalyzer extends ForwardBranchedFlowAnalysis<MyAbstract> {
	
	private String[] varSet;
	private static String resultVarName = "ia_result";
	private static MpqScalar plusInfinity, minusInfinity;
	private static String tempIntervalName = "__temp_interval";
	
	private TrendAnalayzer t;
	
	private int debug = 5;
	

	public IntervalAnalyzer(UnitGraph graph, Chain<Local> a) {
		super(graph);
		
		plusInfinity = new MpqScalar();
		plusInfinity.setInfty(1);
		minusInfinity = new MpqScalar();
		minusInfinity.setInfty(-1);
		
		setVariableSet(a);
		
		
		t = new TrendAnalayzer(4);
		
		doAnalysis();
	}
	
	private void setVariableSet(Chain<Local> a){
		varSet = new String[a.size()];
		int i = 0;
		for (Local l : a) {
			varSet[i] = l.getName();
			i++;
		}
		
	}

	@Override
	protected MyAbstract entryInitialFlow() {
		return MyAbstract.newBottom(varSet, ManagerFactory.newManager());
	}

	@Override
	protected MyAbstract newInitialFlow() {
		return MyAbstract.newBottom(varSet, ManagerFactory.newManager());
	}
	

	@Override
	protected void flowThrough(MyAbstract inState, Unit cmd,
			List<MyAbstract> outState,
			List<MyAbstract> branchOuts) {
		
		//t.analyzeAndWiden(cmd, inState);
		
		if (outState.size() == 0){
			copyStateToAllBranchOuts(inState, branchOuts);
			outState.add(inState);
			return;
		}
		
		try {
			PerformTransformation(inState, cmd, outState.get(0), branchOuts);
		} catch (Exception e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
			return;
		}
		
		if(debug > 3) {
			System.out.println("=================");
			System.out.println("command: " + cmd);
			System.out.println("inState:\n\t" + inState);
			System.out.println("outState:\n\t" + outState);
			System.out.println("branchState:\n\t" + branchOuts);
		}
	}
	
	private void PerformTransformation(MyAbstract inState, Unit cmd, MyAbstract outState, 
			List<MyAbstract> branchOuts) throws Exception {
		
		copy(inState, outState);
		if (cmd instanceof JAssignStmt){
			handleAssignmentStatemnt((JAssignStmt)cmd, outState);
		} else if(cmd instanceof JIfStmt) {
			copyStateToAllBranchOuts(inState, branchOuts);
			handleIfStatemnt((JIfStmt)cmd, outState, branchOuts);
		} 
		else if (commandIsParameterInitializing(cmd)){
			handleIdentityStatemnt((JIdentityStmt)cmd, outState, branchOuts);
		}
		
		t.analyzeAndWiden(cmd, outState);
	}
	
	private void handleIdentityStatemnt(JIdentityStmt cmd, MyAbstract outState,
			List<MyAbstract> branchOuts) {
		
		Value left = cmd.leftBox.getValue();
		Value right = cmd.rightBox.getValue();
		String variableName = extractVariableName(left);
		
		// We ignore the intialization of this.
		if (rightBoxIsThis(right)){
			return;
		}
		
		if (rightBoxIsParameter(right)){
			outState.initVarWithTop(variableName);
		}
	}

	private boolean rightBoxIsParameter(Value right) {
		return right instanceof ParameterRef;
	}

	private boolean rightBoxIsThis(Value right) {
		return right instanceof ThisRef;
	}

	private boolean commandIsParameterInitializing(Unit cmd) {
		return cmd instanceof JIdentityStmt;
	}

	private void copyStateToAllBranchOuts(MyAbstract inState,
			List<MyAbstract> branchOuts) {
		
		for (MyAbstract branch : branchOuts){
			copy(inState, branch);
		}
		
	}

	private void handleIfStatemnt(JIfStmt cmd, MyAbstract outState, List<MyAbstract> branchOuts) {
		
		MyAbstract branchState = branchOuts.get(0);
		Interval outInterval = null, branchInterval = null;
		String op1Name = null;
		
		Value cond_general = cmd.getCondition();
		if(cond_general instanceof AbstractJimpleIntBinopExpr) {
			AbstractJimpleIntBinopExpr cond = (AbstractJimpleIntBinopExpr) cond_general;
			
			op1Name = extractVariableName(cond.getOp1());
			int op2Value = extractValue(cond.getOp2());
			
			if(cond_general instanceof JLeExpr) { // less or equal
				
				branchInterval = new Interval(minusInfinity, new MpqScalar(op2Value));
				outInterval = new Interval(new MpqScalar(op2Value + 1), plusInfinity);
				
			} else if(cond_general instanceof JLtExpr) { //less then
				
				branchInterval = new Interval(minusInfinity, new MpqScalar(op2Value - 1));
				outInterval = new Interval(new MpqScalar(op2Value), plusInfinity);
				
			} else if(cond_general instanceof JGeExpr) { //greater or equal
				
				branchInterval = new Interval(new MpqScalar(op2Value), plusInfinity);
				outInterval = new Interval(minusInfinity, new MpqScalar(op2Value - 1));
				
			} else if(cond_general instanceof JGtExpr) { //greater then
				
				branchInterval = new Interval(new MpqScalar(op2Value + 1), plusInfinity);
				outInterval = new Interval(minusInfinity, new MpqScalar(op2Value));
				
			} else {
				System.err.println("IntervalAnalyzer::handleIfStatemnt - unsupported AbstractJimpleIntBinopExpr class: "
						+ cond_general.getClass());
			}
			
		} else {
			System.err.println("IntervalAnalyzer::handleIfStatemnt - unsupported cond calss: " + cond_general.getClass());
		}
		
		applyConditionOnState(outState, outInterval, op1Name);
		applyConditionOnState(branchState, branchInterval, op1Name);
	}
	
	private void applyConditionOnState(MyAbstract outState, Interval tmpInterval, String op1Name) {
		MyAbstract top = MyAbstract.newTop(varSet, ManagerFactory.newManager());
		top.initVarWithValue(op1Name, tmpInterval);
		outState.meet(top);
	}

	private int extractValue(Value op2) {
		if (op2 instanceof IntConstant){
			IntConstant c = (IntConstant) op2;
			return c.value;
		}
		return 0;
	}

	private void updateMap(HashMap<String, Interval> map, String varName, Interval newInterval) {
		if(!map.containsKey(varName)) {
			System.err.println("IntervalAnalyzer::updateMap got var that is not in map");
			return;
		}
		map.put(varName, newInterval);
	}
	
	private void handleAssignmentStatemnt(JAssignStmt cmd, MyAbstract outState) throws Exception {
		Value nameOfLeft = cmd.leftBox.getValue();
		Value nameOfRight = cmd.rightBox.getValue();
		
		String variableName = extractVariableName(nameOfLeft);
		Linexpr1 xlinexp = createLinearExpression(nameOfRight);
		outState.assign(xlinexp, variableName);
	}

	@Override
	protected void copy(MyAbstract source, MyAbstract dest) {
		dest.copy(source);
	}

	@Override
	protected void merge(MyAbstract source1,
			MyAbstract source2, MyAbstract dest) {
		
		source1.join(source2);
		copy(source1, dest);
	}
	
	
	public static Interval[] getValuesOf(String[] variables, HashMap<String, Interval> state){
		Interval[] result = new Interval[variables.length];
		for (int i = 0 ; i < variables.length ; i++) {
			if (state.containsKey(variables[i])) {
				result[i] = state.get(variables[i]);
			} else {
				result[i] = Utils.newTop();
			}
		}
		return result;
	}
	
	private Linexpr1 createLinearExpression(Value nameOfRight) throws Exception {
		if(nameOfRight instanceof AddExpr) {
			AddExpr addExpr = (AddExpr) nameOfRight;
			return createAddLinearExpression(addExpr.getOp1(), addExpr.getOp2(), false);
			
		} else if(nameOfRight instanceof IntConstant) {
			return createConstLinearExpression((IntConstant) nameOfRight, false);
		} else if(nameOfRight instanceof JimpleLocal) {
			Linterm1[] terms = new Linterm1[] {getLinTermOfLocal(nameOfRight, 1, false)};
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(0));
		} else if(nameOfRight instanceof SubExpr) {
			SubExpr subExpr = (SubExpr) nameOfRight;
			return createAddLinearExpression(subExpr.getOp1(), subExpr.getOp2(), true);
			
		} else if(nameOfRight instanceof MulExpr) {
			MulExpr mulExpr = (MulExpr) nameOfRight;
			return createMulLinearExpression( mulExpr.getOp1(), mulExpr.getOp2());
		} else if(nameOfRight instanceof DivExpr) {
			// not supported!
			return null;
		} else if (nameOfRight instanceof NegExpr){
			NegExpr negExpr = (NegExpr) nameOfRight;
			return createNegLinearExpression(nameOfRight, negExpr);
		} else {
			System.err.println("IntervalAnalyzer::createLinearExpression - unsupporter class of nameOfRight");
			return null;
		}
	}
	
	private Linexpr1 createNegLinearExpression(Value nameOfRight, NegExpr negExpr) {
		Value val = (Value) negExpr.getOp();
		if (operatorLocal(val)){
			Linterm1[] terms = new Linterm1[]{getLinTermOfLocal(val, 1, true)};
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(0));
		}
		else{
			return createConstLinearExpression((IntConstant) nameOfRight, true);
		}
	}

	private boolean operatorLocal(Value val) {
		return val instanceof JimpleLocal;
	}
	
	public static Environment createRelevantExpressionEnvironment2(Linterm1[] terms){
		String[] relevantVarNames = new String[terms.length + 1];
		
		for (int i = 0 ; i < terms.length ; i++){
			relevantVarNames[i] = terms[i].var;
		}
		relevantVarNames[terms.length] = resultVarName;
		return new Environment(relevantVarNames, new String[0]);
	}
	
	public static Environment createRelevantExpressionEnvironment(Linterm1[] terms){
		String[] relevantVarNames = new String[terms.length];
		
		for (int i = 0 ; i < terms.length ; i++){
			relevantVarNames[i] = terms[i].var;
		}
		return new Environment(relevantVarNames, new String[0]);
	}

	private boolean operatorConst(Value val) {
		return val instanceof IntConstant;
	}
	
	private Linexpr1 createMulLinearExpression(Value left, Value right) throws Exception {
		if (bothOperatorsAreConstants(left, right)){
			Linterm1[] terms = new Linterm1[0];
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(getConstantValue(left, false) *  getConstantValue(right, false)));
		}
		else if (firstOperatorLocalSecondConstant(left, right)){
			Linterm1[] terms = new Linterm1[] {getLinTermOfLocal(left, getConstantValue(right, false), false)};
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(0));
		}
		else if (firstOperationConstandSecondOperation(left, right)){
			Linterm1[] terms = new Linterm1[] {getLinTermOfLocal(right, getConstantValue(left, false), false)};
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(0));
		}
		else if (bothOperatorsAreLocals(left, right)){
			throw new Exception("Multiplication between variables is not supported");
			//return new Linexpr1(env, new Linterm1[] {getLinTermOfLocal(left, 1, false), getLinTermOfLocal(right, 1, isSubstract)}, new MpqScalar(0));
		}
		return null;
	}
	
	private Linexpr1 createAddLinearExpression(Value left, Value right, boolean isSubstract) {
		if (bothOperatorsAreConstants(left, right)){
			Linterm1[] terms = new Linterm1[0];
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(getConstantValue(left, false) +  getConstantValue(right, isSubstract)));
		}
		else if (firstOperatorLocalSecondConstant(left, right)){
			Linterm1[] terms = new Linterm1[] {getLinTermOfLocal(left, 1, false)};
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(getConstantValue(right, isSubstract)));
		}
		else if (firstOperationConstandSecondOperation(left, right)){
			Linterm1[] terms = new Linterm1[] {getLinTermOfLocal(right, 1, isSubstract)};
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(getConstantValue(left, false)));
		}
		else if (bothOperatorsAreLocals(left, right)){
			Linterm1[] terms = new Linterm1[] {getLinTermOfLocal(left, 1, false), getLinTermOfLocal(right, 1, isSubstract)};
			return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(0));
		}
		
		return null;
	}
	
	private Linterm1 getLinTermOfLocal(Value op1, int coeff, boolean isNegative) {
		return new Linterm1(((JimpleLocal) op1).getName(), new MpqScalar(isNegative? -coeff : coeff));
	}

	private int getConstantValue(Value op2, boolean isNegative) {
		return isNegative? -((IntConstant) op2).value : ((IntConstant) op2).value;
	}

	private boolean bothOperatorsAreLocals(Value left, Value right) {
		return operatorLocal(left) && operatorLocal(right) ;
	}

	private boolean firstOperationConstandSecondOperation(Value left, Value right) {
		return operatorConst(left) && operatorLocal(right);
	}

	private boolean firstOperatorLocalSecondConstant(Value left, Value right) {
		return operatorLocal(left) && operatorConst(right);
	}

	private boolean bothOperatorsAreConstants(Value left, Value right) {
		return operatorConst(left) && operatorConst(right);
	}

	private Linexpr1 createConstLinearExpression(IntConstant cnst, boolean isNegative) {
		Linterm1[] terms = new Linterm1[0];
		return new Linexpr1(createRelevantExpressionEnvironment(terms), terms, new MpqScalar(cnst.value));
	}
	
	private String extractVariableName(Value nameOfLeft) {
		JimpleLocal a = (JimpleLocal) nameOfLeft;
		return a.getName();
	}
	
	private Interval extractVariableIntreval(Value value, HashMap<String, Interval> map) {
		if(value instanceof IntConstant) {
			int constant = Integer.parseInt(value.toString());
			return new Interval(constant, constant);
		} else if(value instanceof JimpleLocal) {
			return map.get(extractVariableName(value));
		} else {
			System.err.println("IntervalAnalyzer::extractVariableInterval got unknown value type of class " + value.getClass().toString());
			return null;
		}
	}
	
}
